Pointer Subtyping

Some pointer types may be safely used in contexts where another pointer type is expected. In particular, T *@notnull is a subtype of T *@nullable which means that a not-null pointer can be passed anywhere a possibly-null pointer is expected.

Similarly, a T *@numelts(42) pointer can be passed anywhere a T *@numelts(30) pointer is expected, because the former describes sequences that have at least 42 elements, which satisifes the constraint that it has at least 30 elements.

In addition, T*@effect(`r) is a subtype of T*@effect(`r+`s) For example the following code is type-correct:

  void foo(int x) {
    int *@effect(`foo+`H) y = &x;
    y = new 1;
  }

The first assignment is correct since &x is of type int *@effect(`foo) and the type of y states that y is a pointer into the region `foo or into the heap. The second assignment is correct since “new 1” is a heap pointer and y is permitted to point into the heap.

It is possible to specify constraints on effect variables that appear in the parameters of a function as part of the function’s type. For instance, the type of the following function states that the set of regions represented by `r is a subset of the set of regions represented by `s.

  void foobar(int *`r a, int *`s b : `r < `s) {
         b = a;
   }

In general, constraints among the effect variables that appear in a function’s parameters are specified after the arguments in a comma-separated list of constraints separated from that arguments by a colon “:”. In the body of the function foobar above, the assignment is legal since `r is guaranteed to be a subset of `s. (We support another form of constraint “single(`e)” which states that the set of regions represented by `e must be a singleton. This is described further in the section “Pointers with Restricted Aliasing”.)

Finally, when T is a subtype of S, then T* is a subtype of const S*. So, for instance, if we declare:

// nullable int pointers
typedef int * nintptr_t;
// not-nullable int pointers
typedef int *@notnull intptr_t;

then intptr_t * is a subtype of const nintptr_t *. Note, however, that “const” is important to get this kind of deep subtyping.

The following example shows what could go wrong if we allowed deep subtyping without the const:

  void f(int *@notnull *@notnull x) {
    int *@nullable *@notnull y = x; 
    // would be legal if int *@nullable *@notnull 
    // was a subtype of int *@notnull *@notnull.
    *y = NULL;    
    // legal because *y has type int *@nullable
    **x;          
    // seg faults even though the type of *x is 
    // int *@notnull
  }